\begin{tabbing}
sumdeq($a$; $b$)($p$,$q$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=case $p$\+
\\[0ex]o\=f inl(${\it pa}$) =$>$ case $q$ of inl(${\it qa}$) =$>$ ($a$.1)(${\it pa}$,${\it qa}$) $\mid$ inr(${\it qb}$) =$>$ ff\+
\\[0ex]$\mid$ inr(${\it pb}$) =$>$ case $q$ of inl(${\it qa}$) =$>$ ff $\mid$ inr(${\it qb}$) =$>$ ($b$.1)(${\it pb}$,${\it qb}$)
\-\-
\end{tabbing}